Nuprl Definition : update-spec-join
0,22
postcript
pdf
a
b
==
a
b
latex
clarification:
a
b
== fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);
a
;
b
)
latex
Definitions
f
g
,
product-deq(
A
;
B
;
a
;
b
)
,
Knd
,
Id
,
KindDeq
,
IdDeq
FDL editor aliases
update-spec-join
origin
b == a b
b == fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);a;b) b == a b
b == fpf-join(product-deq(Knd;Id;KindDeq;IdDeq);a;b) g